/-
Copyright (c) 2020 Sébastien Gouëzel. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sébastien Gouëzel
-/
module

public import Mathlib.Topology.UniformSpace.UniformConvergence

/-!
# Locally uniform convergence

We define a sequence of functions `Fₙ` to *converge locally uniformly* to a limiting function `f`
with respect to a filter `p`, spelled `TendstoLocallyUniformly F f p`, if for any `x ∈ s` and any
entourage of the diagonal `u`, there is a neighbourhood `v` of `x` such that `p`-eventually we have
`(f y, Fₙ y) ∈ u` for all `y ∈ v`.

It is important to note that this definition is somewhat non-standard; it is **not** in general
equivalent to "every point has a neighborhood on which the convergence is uniform", which is the
definition more commonly encountered in the literature. The reason is that in our definition the
neighborhood `v` of `x` can depend on the entourage `u`; so our condition is *a priori* weaker than
the usual one, although the two conditions are equivalent if the domain is locally compact. See
`tendstoLocallyUniformlyOn_of_forall_exists_nhds` for the one-way implication; the equivalence
assuming local compactness is part of `tendstoLocallyUniformlyOn_TFAE`.

We adopt this weaker condition because it is more general but appears to be sufficient for
the standard applications of locally-uniform convergence (in particular, for proving that a
locally-uniform limit of continuous functions is continuous).

We also define variants for locally uniform convergence on a subset, called
`TendstoLocallyUniformlyOn F f p s`.

## Tags

Uniform limit, uniform convergence, tends uniformly to
-/

@[expose] public section

noncomputable section

open Topology Uniformity Filter Set Uniform

variable {α β γ ι : Type*} [TopologicalSpace α] [UniformSpace β]
variable {F : ι → α → β} {f : α → β} {s s' : Set α} {x : α} {p : Filter ι}

/-- A sequence of functions `Fₙ` converges locally uniformly on a set `s` to a limiting function
`f` with respect to a filter `p` if, for any entourage of the diagonal `u`, for any `x ∈ s`, one
has `p`-eventually `(f y, Fₙ y) ∈ u` for all `y` in a neighborhood of `x` in `s`. -/
def TendstoLocallyUniformlyOn (F : ι → α → β) (f : α → β) (p : Filter ι) (s : Set α) :=
  ∀ u ∈ 𝓤 β, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ n in p, ∀ y ∈ t, (f y, F n y) ∈ u

/-- A sequence of functions `Fₙ` converges locally uniformly to a limiting function `f` with respect
to a filter `p` if, for any entourage of the diagonal `u`, for any `x`, one has `p`-eventually
`(f y, Fₙ y) ∈ u` for all `y` in a neighborhood of `x`. -/
def TendstoLocallyUniformly (F : ι → α → β) (f : α → β) (p : Filter ι) :=
  ∀ u ∈ 𝓤 β, ∀ x : α, ∃ t ∈ 𝓝 x, ∀ᶠ n in p, ∀ y ∈ t, (f y, F n y) ∈ u

theorem tendstoLocallyUniformlyOn_univ :
    TendstoLocallyUniformlyOn F f p univ ↔ TendstoLocallyUniformly F f p := by
  simp [TendstoLocallyUniformlyOn, TendstoLocallyUniformly, nhdsWithin_univ]

theorem tendstoLocallyUniformlyOn_iff_forall_tendsto :
    TendstoLocallyUniformlyOn F f p s ↔
      ∀ x ∈ s, Tendsto (fun y : ι × α => (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β) :=
  forall₂_swap.trans <| forall₄_congr fun _ _ _ _ => by
    simp_rw [mem_map, mem_prod_iff_right, mem_preimage]

nonrec theorem IsOpen.tendstoLocallyUniformlyOn_iff_forall_tendsto (hs : IsOpen s) :
    TendstoLocallyUniformlyOn F f p s ↔
      ∀ x ∈ s, Tendsto (fun y : ι × α => (f y.2, F y.1 y.2)) (p ×ˢ 𝓝 x) (𝓤 β) :=
  tendstoLocallyUniformlyOn_iff_forall_tendsto.trans <| forall₂_congr fun x hx => by
    rw [hs.nhdsWithin_eq hx]

theorem tendstoLocallyUniformly_iff_forall_tendsto :
    TendstoLocallyUniformly F f p ↔
      ∀ x, Tendsto (fun y : ι × α => (f y.2, F y.1 y.2)) (p ×ˢ 𝓝 x) (𝓤 β) := by
  simp [← tendstoLocallyUniformlyOn_univ, isOpen_univ.tendstoLocallyUniformlyOn_iff_forall_tendsto]

theorem tendstoLocallyUniformlyOn_iff_tendstoLocallyUniformly_comp_coe :
    TendstoLocallyUniformlyOn F f p s ↔
      TendstoLocallyUniformly (fun i (x : s) => F i x) (f ∘ (↑)) p := by
  simp only [tendstoLocallyUniformly_iff_forall_tendsto, Subtype.forall', tendsto_map'_iff,
    tendstoLocallyUniformlyOn_iff_forall_tendsto, ← map_nhds_subtype_val, prod_map_right]; rfl

protected theorem TendstoUniformlyOn.tendstoLocallyUniformlyOn (h : TendstoUniformlyOn F f p s) :
    TendstoLocallyUniformlyOn F f p s := fun u hu _ _ =>
  ⟨s, self_mem_nhdsWithin, by simpa using h u hu⟩

protected theorem TendstoUniformly.tendstoLocallyUniformly (h : TendstoUniformly F f p) :
    TendstoLocallyUniformly F f p := fun u hu _ => ⟨univ, univ_mem, by simpa using h u hu⟩

theorem TendstoLocallyUniformlyOn.mono (h : TendstoLocallyUniformlyOn F f p s) (h' : s' ⊆ s) :
    TendstoLocallyUniformlyOn F f p s' := by
  intro u hu x hx
  rcases h u hu x (h' hx) with ⟨t, ht, H⟩
  exact ⟨t, nhdsWithin_mono x h' ht, H.mono fun n => id⟩

theorem tendstoLocallyUniformlyOn_iUnion {ι' : Sort*} {S : ι' → Set α} (hS : ∀ i, IsOpen (S i))
    (h : ∀ i, TendstoLocallyUniformlyOn F f p (S i)) :
    TendstoLocallyUniformlyOn F f p (⋃ i, S i) :=
  (isOpen_iUnion hS).tendstoLocallyUniformlyOn_iff_forall_tendsto.2 fun _x hx =>
    let ⟨i, hi⟩ := mem_iUnion.1 hx
    (hS i).tendstoLocallyUniformlyOn_iff_forall_tendsto.1 (h i) _ hi

theorem tendstoLocallyUniformlyOn_biUnion {s : Set γ} {S : γ → Set α} (hS : ∀ i ∈ s, IsOpen (S i))
    (h : ∀ i ∈ s, TendstoLocallyUniformlyOn F f p (S i)) :
    TendstoLocallyUniformlyOn F f p (⋃ i ∈ s, S i) :=
  tendstoLocallyUniformlyOn_iUnion (fun i => isOpen_iUnion (hS i))
    fun i ↦ tendstoLocallyUniformlyOn_iUnion (hS i) (h i)

theorem tendstoLocallyUniformlyOn_sUnion (S : Set (Set α)) (hS : ∀ s ∈ S, IsOpen s)
    (h : ∀ s ∈ S, TendstoLocallyUniformlyOn F f p s) : TendstoLocallyUniformlyOn F f p (⋃₀ S) := by
  rw [sUnion_eq_biUnion]
  exact tendstoLocallyUniformlyOn_biUnion hS h

theorem TendstoLocallyUniformlyOn.union (hs₁ : IsOpen s) (hs₂ : IsOpen s')
    (h₁ : TendstoLocallyUniformlyOn F f p s) (h₂ : TendstoLocallyUniformlyOn F f p s') :
    TendstoLocallyUniformlyOn F f p (s ∪ s') := by
  rw [← sUnion_pair]
  refine tendstoLocallyUniformlyOn_sUnion _ ?_ ?_ <;> simp [*]

protected theorem TendstoLocallyUniformly.tendstoLocallyUniformlyOn
    (h : TendstoLocallyUniformly F f p) : TendstoLocallyUniformlyOn F f p s :=
  (tendstoLocallyUniformlyOn_univ.mpr h).mono (subset_univ _)

/-- On a compact space, locally uniform convergence is just uniform convergence. -/
theorem tendstoLocallyUniformly_iff_tendstoUniformly_of_compactSpace [CompactSpace α] :
    TendstoLocallyUniformly F f p ↔ TendstoUniformly F f p := by
  refine ⟨fun h V hV => ?_, TendstoUniformly.tendstoLocallyUniformly⟩
  choose U hU using h V hV
  obtain ⟨t, ht⟩ := isCompact_univ.elim_nhds_subcover' (fun k _ => U k) fun k _ => (hU k).1
  replace hU := fun x : t => (hU x).2
  rw [← eventually_all] at hU
  refine hU.mono fun i hi x => ?_
  specialize ht (mem_univ x)
  simp only [exists_prop, mem_iUnion, SetCoe.exists, exists_and_right] at ht
  obtain ⟨y, ⟨hy₁, hy₂⟩, hy₃⟩ := ht
  exact hi ⟨⟨y, hy₁⟩, hy₂⟩ x hy₃

/-- For a compact set `s`, locally uniform convergence on `s` is just uniform convergence on `s`. -/
theorem tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact (hs : IsCompact s) :
    TendstoLocallyUniformlyOn F f p s ↔ TendstoUniformlyOn F f p s := by
  haveI : CompactSpace s := isCompact_iff_compactSpace.mp hs
  refine ⟨fun h => ?_, TendstoUniformlyOn.tendstoLocallyUniformlyOn⟩
  rwa [tendstoLocallyUniformlyOn_iff_tendstoLocallyUniformly_comp_coe,
    tendstoLocallyUniformly_iff_tendstoUniformly_of_compactSpace, ←
    tendstoUniformlyOn_iff_tendstoUniformly_comp_coe] at h

theorem TendstoLocallyUniformlyOn.comp [TopologicalSpace γ] {t : Set γ}
    (h : TendstoLocallyUniformlyOn F f p s) (g : γ → α) (hg : MapsTo g t s)
    (cg : ContinuousOn g t) : TendstoLocallyUniformlyOn (fun n => F n ∘ g) (f ∘ g) p t := by
  intro u hu x hx
  rcases h u hu (g x) (hg hx) with ⟨a, ha, H⟩
  have : g ⁻¹' a ∈ 𝓝[t] x :=
    (cg x hx).preimage_mem_nhdsWithin' (nhdsWithin_mono (g x) hg.image_subset ha)
  exact ⟨g ⁻¹' a, this, H.mono fun n hn y hy => hn _ hy⟩

theorem TendstoLocallyUniformly.comp [TopologicalSpace γ] (h : TendstoLocallyUniformly F f p)
    (g : γ → α) (cg : Continuous g) : TendstoLocallyUniformly (fun n => F n ∘ g) (f ∘ g) p := by
  rw [← tendstoLocallyUniformlyOn_univ] at h ⊢
  rw [← continuousOn_univ] at cg
  exact h.comp _ (mapsTo_univ _ _) cg

/-- If every `x ∈ s` has a neighbourhood within `s` on which `F i` tends uniformly to `f`, then
`F i` tends locally uniformly on `s` to `f`.

Note this is **not** a tautology, since our definition of `TendstoLocallyUniformlyOn` is slightly
more general (although the conditions are equivalent if `β` is locally compact and `s` is open,
see `tendstoLocallyUniformlyOn_TFAE`). -/
lemma tendstoLocallyUniformlyOn_of_forall_exists_nhds
    (h : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, TendstoUniformlyOn F f p t) :
    TendstoLocallyUniformlyOn F f p s := by
  refine tendstoLocallyUniformlyOn_iff_forall_tendsto.mpr fun x hx ↦ ?_
  obtain ⟨t, ht, htr⟩ := h x hx
  rw [tendstoUniformlyOn_iff_tendsto] at htr
  exact htr.mono_left <| prod_mono_right _ <| le_principal_iff.mpr ht

@[deprecated (since := "2025-05-22")] alias tendstoLocallyUniformlyOn_of_forall_exists_nhd :=
  tendstoLocallyUniformlyOn_of_forall_exists_nhds

/-- If every `x` has a neighbourhood on which `F i` tends uniformly to `f`, then `F i` tends
locally uniformly to `f`. (Special case of `tendstoLocallyUniformlyOn_of_forall_exists_nhds`
where `s = univ`.) -/
lemma tendstoLocallyUniformly_of_forall_exists_nhds
    (h : ∀ x, ∃ t ∈ 𝓝 x, TendstoUniformlyOn F f p t) :
    TendstoLocallyUniformly F f p :=
  tendstoLocallyUniformlyOn_univ.mp
    <| tendstoLocallyUniformlyOn_of_forall_exists_nhds (by simpa using h)

@[deprecated (since := "2025-05-22")] alias tendstoLocallyUniformly_of_forall_exists_nhd :=
  tendstoLocallyUniformly_of_forall_exists_nhds

theorem tendstoLocallyUniformlyOn_TFAE [LocallyCompactSpace α] (G : ι → α → β) (g : α → β)
    (p : Filter ι) (hs : IsOpen s) :
    List.TFAE [
      TendstoLocallyUniformlyOn G g p s,
      ∀ K, K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K,
      ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v] := by
  tfae_have 1 → 2
  | h, K, hK1, hK2 =>
    (tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact hK2).mp (h.mono hK1)
  tfae_have 2 → 3
  | h, x, hx => by
    obtain ⟨K, ⟨hK1, hK2⟩, hK3⟩ := (compact_basis_nhds x).mem_iff.mp (hs.mem_nhds hx)
    exact ⟨K, nhdsWithin_le_nhds hK1, h K hK3 hK2⟩
  tfae_have 3 → 1
  | h, u, hu, x, hx => by
    obtain ⟨v, hv1, hv2⟩ := h x hx
    exact ⟨v, hv1, hv2 u hu⟩
  tfae_finish

theorem tendstoLocallyUniformlyOn_iff_forall_isCompact [LocallyCompactSpace α] (hs : IsOpen s) :
    TendstoLocallyUniformlyOn F f p s ↔ ∀ K, K ⊆ s → IsCompact K → TendstoUniformlyOn F f p K :=
  (tendstoLocallyUniformlyOn_TFAE F f p hs).out 0 1

lemma tendstoLocallyUniformly_iff_forall_isCompact [LocallyCompactSpace α] :
    TendstoLocallyUniformly F f p ↔ ∀ K : Set α, IsCompact K → TendstoUniformlyOn F f p K := by
  simp only [← tendstoLocallyUniformlyOn_univ,
    tendstoLocallyUniformlyOn_iff_forall_isCompact isOpen_univ, Set.subset_univ, forall_true_left]

theorem tendstoLocallyUniformlyOn_iff_filter :
    TendstoLocallyUniformlyOn F f p s ↔ ∀ x ∈ s, TendstoUniformlyOnFilter F f p (𝓝[s] x) := by
  simp only [TendstoUniformlyOnFilter, eventually_prod_iff]
  constructor
  · rintro h x hx u hu
    obtain ⟨s, hs1, hs2⟩ := h u hu x hx
    exact ⟨_, hs2, _, eventually_of_mem hs1 fun x => id, fun hi y hy => hi y hy⟩
  · rintro h u hu x hx
    obtain ⟨pa, hpa, pb, hpb, h⟩ := h x hx u hu
    exact ⟨pb, hpb, eventually_of_mem hpa fun i hi y hy => h hi hy⟩

theorem tendstoLocallyUniformly_iff_filter :
    TendstoLocallyUniformly F f p ↔ ∀ x, TendstoUniformlyOnFilter F f p (𝓝 x) := by
  simpa [← tendstoLocallyUniformlyOn_univ, ← nhdsWithin_univ] using
    @tendstoLocallyUniformlyOn_iff_filter _ _ _ _ _ F f univ p

theorem TendstoLocallyUniformlyOn.tendsto_at (hf : TendstoLocallyUniformlyOn F f p s) {a : α}
    (ha : a ∈ s) : Tendsto (fun i => F i a) p (𝓝 (f a)) := by
  refine ((tendstoLocallyUniformlyOn_iff_filter.mp hf) a ha).tendsto_at ?_
  simpa only [Filter.principal_singleton] using pure_le_nhdsWithin ha

theorem TendstoLocallyUniformlyOn.unique [p.NeBot] [T2Space β] {g : α → β}
    (hf : TendstoLocallyUniformlyOn F f p s) (hg : TendstoLocallyUniformlyOn F g p s) :
    s.EqOn f g := fun _a ha => tendsto_nhds_unique (hf.tendsto_at ha) (hg.tendsto_at ha)

theorem TendstoLocallyUniformlyOn.congr_inseparable {G : ι → α → β}
    (hf : TendstoLocallyUniformlyOn F f p s)
    (hg : ∀ᶠ n in p, ∀ x ∈ s, Inseparable (F n x) (G n x)) : TendstoLocallyUniformlyOn G f p s := by
  have hg : ∀ᶠ x in p ×ˢ 𝓟 s, Inseparable (F x.1 x.2) (G x.1 x.2) := by
    simpa using eventually_prod_principal_iff.2 hg
  rw [tendstoLocallyUniformlyOn_iff_forall_tendsto] at hf ⊢
  refine forall₂_imp (fun x hx hf => ?_) hf
  rw [uniformity_hasBasis_open.tendsto_right_iff] at hf ⊢
  exact fun i hi => (hf i hi).mp ((hg.filter_mono (prod_mono_right p inf_le_right)).mono
    fun x hg hf => ((Inseparable.rfl.prod hg).mem_open_iff hi.2).1 hf)

theorem TendstoLocallyUniformlyOn.congr {G : ι → α → β} (hf : TendstoLocallyUniformlyOn F f p s)
    (hg : ∀ n, s.EqOn (F n) (G n)) : TendstoLocallyUniformlyOn G f p s :=
  hf.congr_inseparable (.of_forall fun n _ hx => .of_eq (hg n hx))

theorem TendstoLocallyUniformlyOn.congr_inseparable_right {g : α → β}
    (hf : TendstoLocallyUniformlyOn F f p s)
    (hg : ∀ x ∈ s, Inseparable (f x) (g x)) : TendstoLocallyUniformlyOn F g p s := by
  have hg : ∀ᶠ x in p ×ˢ 𝓟 s, Inseparable (f x.2) (g x.2) := by
    rw [eventually_prod_principal_iff]
    exact .of_forall fun _ => hg
  rw [tendstoLocallyUniformlyOn_iff_forall_tendsto] at hf ⊢
  refine forall₂_imp (fun x hx hf => ?_) hf
  rw [uniformity_hasBasis_open.tendsto_right_iff] at hf ⊢
  exact fun i hi => (hf i hi).mp ((hg.filter_mono (prod_mono_right p inf_le_right)).mono
    fun x hg hf => ((hg.prod .rfl).mem_open_iff hi.2).1 hf)

theorem TendstoLocallyUniformlyOn.congr_right {g : α → β} (hf : TendstoLocallyUniformlyOn F f p s)
    (hg : s.EqOn f g) : TendstoLocallyUniformlyOn F g p s :=
  hf.congr_inseparable_right fun _ hx => .of_eq (hg hx)

theorem TendstoLocallyUniformly.congr_inseparable {G : ι → α → β}
    (hf : TendstoLocallyUniformly F f p)
    (hg : ∀ᶠ n in p, ∀ x, Inseparable (F n x) (G n x)) : TendstoLocallyUniformly G f p :=
  tendstoLocallyUniformlyOn_univ.1
    (hf.tendstoLocallyUniformlyOn.congr_inseparable (by simpa using hg))

theorem TendstoLocallyUniformly.congr {G : ι → α → β} (hf : TendstoLocallyUniformly F f p)
    (hg : ∀ n x, F n x = G n x) : TendstoLocallyUniformly G f p :=
  hf.congr_inseparable (.of_forall fun n x => .of_eq (hg n x))

theorem TendstoLocallyUniformly.congr_inseparable_right {g : α → β}
    (hf : TendstoLocallyUniformly F f p)
    (hg : ∀ x, Inseparable (f x) (g x)) : TendstoLocallyUniformly F g p :=
  tendstoLocallyUniformlyOn_univ.1
    (hf.tendstoLocallyUniformlyOn.congr_inseparable_right (by simpa using hg))

theorem TendstoLocallyUniformly.congr_right {g : α → β} (hf : TendstoLocallyUniformly F f p)
    (hg : ∀ x, f x = g x) : TendstoLocallyUniformly F g p :=
  hf.congr_inseparable_right fun x => .of_eq (hg x)
